package org.barad.architecture.analyzer.model.impl;

import java.lang.reflect.Field;
import java.util.ArrayList;
import java.util.List;

import kodkod.ast.Formula;
import kodkod.ast.Relation;
import kodkod.ast.Variable;
import kodkod.ast.QuantifiedFormula.Quantifier;
import kodkod.engine.Solution;
import kodkod.engine.Solver;
import kodkod.engine.satlab.SATFactory;
import kodkod.instance.Bounds;
import kodkod.instance.Tuple;
import kodkod.instance.TupleFactory;
import kodkod.instance.TupleSet;
import kodkod.instance.Universe;

@SuppressWarnings("unused")
public class SoftwareArchitectureModel extends SoftwareArchitectureModelBase {
	
	/*
	 * //name of a component
	 * sig Name {}
	 */
	private Relation name = Relation.unary("Name");
	private TupleSet nameSet;
	
	/*
	 * //constraint
     * sig Constraint{}
	 */
	private Relation constraint = Relation.unary("Constraint");
	private TupleSet constraintSet;
    
	/*
     * //specification for dependencies/services
	 * sig Specification {
	 * input: set 	Constraint,
	 * output: set Constraint,
	 * general: set Constraint 
     * }
     */
	private Relation specification = Relation.unary("Specification");
	private TupleSet specificationSet;
	private Relation input = Relation.binary("Input");
	private TupleSet inputSet;
	private Relation output = Relation.binary("Output");
	private TupleSet outputSet;
	private Relation general = Relation.binary("General");
	private TupleSet generalSet;
	
    /*
     * //all constraints are in the specification
     * fact AllConstrainsInSpecification {
	 * Constraint in Specification.input + Specification.output + Specification.general
     * }
     */
	public Formula AllConstrainsInSpecification() {
		Variable c = Variable.unary("c");
		return c.in(specification.join(input)
				.union(specification.join(output))
				.union(specification.join(general)))
				.forAll(c.oneOf(constraint));
	}

	/*
	 * //should give a counterexample - OK (see below)
	 * assert TestAllConstrainsInSpecification {
	 * some c: Constraint | not c in Specification.input & Specification.output & Specification.general
     * }
	 */
	public Formula TestAllConstrainsInSpecification() {
		Variable c = Variable.unary("c");
		return c.in(specification.join(input)
				.intersection(specification.join(output))
				.intersection(specification.join(general)))
				.not().forSome(c.oneOf(constraint));
	}
	
	/*
	 * Test if AllConstrainsInSpecification is valid - should find a counterexample -OK
	 */
	public Formula VerifyAllConstrainsInSpecification() {
		return AllConstrainsInSpecification().and(TestAllConstrainsInSpecification());
	}
	
	/*
	 * //architectural element
	 * abstract sig ArchitecturalElement {
	 * name:  one Name,
	 * services: set Specification, //ServiceSpecification,
	 * dependencies: set Specification, //DependencySpecification, 
	 * neighbour: set ArchitecturalElement
     * } 
	 */
	private Relation architecturalElement = Relation.unary("ArchitecturalElement");
	private TupleSet architecturalelementSet;
	private Relation architecturalElementName = Relation.binary("ArchitecturalElementName");
	private TupleSet architecturalelementnameSet;
	private Relation service = Relation.binary("Service");
	private TupleSet serviceSet;
	private Relation dependency = Relation.binary("Dependency");
	private TupleSet dependencySet;
	private Relation neighbor = Relation.binary("Neighbor");
	private TupleSet neighborSet;
	
	/*
	 * //processing element
	 * sig Processing extends ArchitecturalElement {}
	 */
	private Relation processing = Relation.unary("Processing");
	private TupleSet processingSet;
	
	/*
	 * //data element
	 * sig Data extends ArchitecturalElement {}
	 */
	private Relation data = Relation.unary("Data");
	private TupleSet dataSet;
	
	/*
	 * //connector element
	 * sig Connector extends ArchitecturalElement {}
	 */
	private Relation connector = Relation.unary("Connector");
	private TupleSet connectorSet;
	
	/*
	 * //no common entities
	 * fact NoCommonEntities {
	 * //no common names
	 * name in ArchitecturalElement one -> one Name
	 * //no common services specifications
	 * services in ArchitecturalElement one -> set Specification
	 * //no common dependencies specifications
	 * dependencies in ArchitecturalElement one -> set Specification
     * }
	 */
	public Formula NoCommonEntities() {
		Variable spec1 = Variable.unary("spec1");
		Variable archElem1 = Variable.unary("archElem1");
		//no common names
		Formula noCommonNames = architecturalElementName.in(archElem1.product(spec1)).forAll(archElem1.oneOf(architecturalElement).and(spec1.oneOf(name)));
		Variable spec2 = Variable.unary("spec2");
		Variable archElem2 = Variable.unary("architecturalElement2");
		//no common services specifications
		//TODO: Tth formula below at the end it should be set???
		Formula noCommonServiceSpecifications = service.in(archElem2.product(spec2)).forAll(archElem2.oneOf(architecturalElement)).forSome(spec2.someOf(specification));
		Variable spec3 = Variable.unary("spec3");
		Variable archElem3 = Variable.unary("archElem3");
		//no common dependencies specifications
		Formula noCommonDependencySpecifications = dependency.in(archElem3.product(spec3)).forAll(archElem3.oneOf(architecturalElement)).forSome(spec3.setOf(specification));                                              
		return noCommonNames.and(noCommonServiceSpecifications).and(noCommonDependencySpecifications);
	}
	
	/**
	 * Create atoms and set bounds for each relation in the model
	 * @param scope The scope for the entire model
	 * @return New bounds instance
	 */
	public Bounds allBounds(int scope) {
		List<String> atoms = new ArrayList<String>(scope);
		addAtomsToUniverse(name.toString(), atoms, scope);
		addAtomsToUniverse(constraint.toString(), atoms, scope);
		addAtomsToUniverse(specification.toString(), atoms, scope);
		addAtomsToUniverse(input.toString(), atoms, scope);
		addAtomsToUniverse(output.toString(), atoms, scope);
		addAtomsToUniverse(general.toString(), atoms, scope);
		addAtomsToUniverse(architecturalElement.toString(), atoms, scope);
		addAtomsToUniverse(architecturalElementName.toString(), atoms, scope);
		addAtomsToUniverse(service.toString(), atoms, scope);
		addAtomsToUniverse(dependency.toString(), atoms, scope);
		addAtomsToUniverse(neighbor.toString(), atoms, scope);
		addAtomsToUniverse(processing.toString(), atoms, scope);
		addAtomsToUniverse(data.toString(), atoms, scope);
		addAtomsToUniverse(connector.toString(), atoms, scope);
		Universe universe = new Universe(atoms);
		TupleFactory factory = universe.factory();
		Bounds bounds = new Bounds(universe);
		int max = scope - 1;
		boundRangefOfUnaryRelation(name, bounds, factory, 0, max - 1);
		boundRangefOfUnaryRelation(constraint, bounds, factory, 0, max - 1);
		boundRangefOfUnaryRelation(specification, bounds, factory, 0, max - 1);
		boundRangeOfBinaryRelation(input, constraintSet, bounds, factory, 0, max - 1);
		boundRangeOfBinaryRelation(output, constraintSet, bounds, factory, 0, max - 1);
		boundRangeOfBinaryRelation(general, constraintSet, bounds, factory, 0, max - 1);
		boundRangefOfUnaryRelation(architecturalElement, bounds, factory, 0, max - 1);
		boundRangeOfBinaryRelation(architecturalElementName, nameSet, bounds, factory, 0, max - 1);
		boundRangeOfBinaryRelation(service, specificationSet, bounds, factory, 0, max - 1);
		boundRangeOfBinaryRelation(dependency, specificationSet, bounds, factory, 0, max - 1);
		boundRangeOfBinaryRelation(neighbor, architecturalelementSet, bounds, factory, 0, max - 1);
		boundRangefOfUnaryRelation(processing, bounds, factory, 0, max - 1);
		boundRangefOfUnaryRelation(data, bounds, factory, 0, max - 1);
		boundRangefOfUnaryRelation(connector, bounds, factory, 0, max - 1);
		return bounds;
	}
	
	//run the model
	public static void main(String[] args) {
		Solver solver = new Solver();
		solver.options().setSolver(SATFactory.LightSAT4J);
		SoftwareArchitectureModel sa = new SoftwareArchitectureModel();
		Solution solution = solver.solve(sa.AllConstrainsInSpecification(), sa.allBounds(5));
		//Solution solution = solver.solve(sa.NoCommonEntities(), sa.allBounds(7));
		System.out.println(solution);
	}
}

























